i,x:Id, T:Type, ds:fpf(Id; x.Type), f:((decl-state(ds)Tdecl-type{i:l}
i,x:Id, T:Type, ds:fpf(Id; x.Type), f:((decl-state(ds)Tdecl-type(ds; x)) + (decl-state(ds)T
i,x:Id, T:Type, ds:fpf(Id; x.Type), f:(rationalsdecl-type{i:l}
i,x:Id, T:Type, ds:fpf(Id; x.Type), f:(rationalsdecl-type(ds; x))),
k:Knd, A:es_realizer{i:l}.
R-Feasible{i:l}
R-Feasible(A)
 ((R-occurs(A; i; x)))
 fpf-compatible(Id; x.Type; id-deq; ds; R-ds(A; i))
 fpf-compatible(Knd; k.Type; Kind-deq; fpf-single(k; T); R-da(A; i))
 ((isrcv(k))  subtype_rel(fpf-cap(R-da(A; source(lnk(k))); Kind-deq; k; void); T))
 ((write-restricted(A; i; k)))
 (y:Id. (fpf-dom(id-deq; y; ds))  ((read-restricted(A; i; y))))
 R-compat{i:l}
 R-compat(Reffect(i; ds; k; T; x; f); A) 

latex

Definitions

outl(x), x(s), rcv(l,tg), tag(k), T, top, let x = a in b(x), A c B, bor(p; q), b, P  Q, P  Q, P  Q, read-restricted(R; i; y), write-restricted(R; i; k), R-da(R; i), R-ds(R; i), R-occurs(R; i; z), A, R-Feasible{i:l}(R), Rinit-v(x1), Reffect-f(x1), Rinit-discrete(A), Rinit-x(x1), Rinit?(x1), Reffect-discrete(A), guard(T), sq_type(T), x. t(x), prop{i:l}, Rsends-T(x1), Reffect-T(x1), Rsends-dt(x1), Rpre-a(x1), Rpre-ds(x1), Rpre?(x1), Rsends-ds(x1), Rbframe-L(x1), Rbframe-k(x1), Rbframe?(x1), Rsframe-L(x1), Rsends-knd(x1), Rsends-g(x1), Rsframe-tag(x1), Rsends-l(x1), Rsframe-lnk(x1), Rsframe?(x1), Rsends?(x1), Rrframe-L(x1), Reffect-ds(x1), Rrframe-x(x1), Rrframe?(x1), Raframe-L(x1), Raframe-k(x1), Raframe?(x1), Rframe-L(x1), Reffect-knd(x1), Reffect-x(x1), Rframe-x(x1), Rframe?(x1), Reffect?(x1), tt, t.2, (i = j), R-interface-compat(A; B), R-discrete_compat(A; B), R-frame-compat(A; B), R-base-domain(R), eq_bd(p; q), Rda(R), Rds(R), R-loc(R), Rnone?(x1), Rplus-right(x1), Rplus-left(x1), P  Q, Rplus?(x1), True, band(p; q), Y, ff, t.1, if b then t else f fi , t  T, R-compat{i:l}(A; B), P  Q, x:A. B(x), False, reduce(f; k; as), deq-member(eq; x; L), fpf-empty, , Unit, fpf-dom(eq; x; f), fpf-cap(f; eq; x; z), es_realizer{i:l}, Rrframe(loc; x; L), Rbframe(loc; k; L), Raframe(loc; k; L), Rpre(loc; ds; a; p; P), Rsends(ds; knd; T; l; dt; g), Rsframe(lnk; tag; L), Rframe(loc; T; x; L), Rinit(loc; T; x; v), Rplus(left; right), Rnone, , Reffect(loc; ds; knd; T; x; f), eq_knd(a; b)

Lemmas

assert-deq-member, l member wf, deq-member wf, tagof wf, lnk-decl-cap, isrcv-implies, squash wf, Knd sq, bool sq, bool cases, fpf-cap-single, lnk-decl wf, top wf, fpf-single wf, fpf-join-cap, IdLnk sq, assert-eq-lnk, eq lnk wf, Rsends wf, or functionality wrt iff, and functionality wrt iff, assert of band, true wf, btrue wf, band wf, assert-eq-knd, eq knd wf, fpf-sub-join-right, fpf-sub-join-left, subtype-fpf-cap-void, subtype rel transitivity, R-compat-ds, R-compat-da, fpf-compatible-join-iff, all functionality wrt iff, assert of bor, fpf-join wf, bor wf, R-compat-Rplus2, Reffect wf, R-compat wf, subtype rel wf, implies functionality wrt iff, Id wf, fpf wf, es realizer wf, Rbframe wf, Rpre wf, Rsframe wf, Rframe wf, Rinit wf, assert of bnot, eqff to assert, bnot wf, not functionality wrt iff, eq id self, Id sq, assert-eq-id, eqtt to assert, iff transitivity, eq id wf, R-Feasible wf, R-occurs wf, R-ds wf, fpf-single wf3, fpf-compatible wf, Kind-deq wf, lnk wf, lsrc wf, R-da wf, fpf-cap wf, isrcv wf, write-restricted wf, Rnone wf, read-restricted wf, not wf, fpf-trivial-subtype-top, id-deq wf, fpf-dom wf, assert wf, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, Knd wf, IdLnk wf, rationals wf, unit wf